\documentclass[10pt, a4paper]{article}
\usepackage[paper=a4paper, left=1.5cm, right=1.5cm, bottom=1.5cm, top=3.5cm]{geometry}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[spanish]{babel}
\usepackage{indentfirst}
\usepackage{fancyhdr}
\usepackage{latexsym}
\usepackage{lastpage}
\usepackage{aed2-symb,aed2-itef,aed2-tad}
\usepackage[colorlinks=true, linkcolor=blue]{hyperref}
\usepackage{calc}

\newcommand{\f}[1]{\text{#1}}
\renewcommand{\paratodo}[2]{$\forall~#2$: #1}

\sloppy

\hypersetup{%
 % Para que el PDF se abra a pgina completa.
 pdfstartview= {FitH \hypercalcbp{\paperheight-\topmargin-1in-\headheight}},
 pdfauthor={Ctedra de Algoritmos y Estructuras de Datos II - DC - UBA},
 pdfkeywords={TADs bsicos},
 pdfsubject={Tipos abstractos de datos bsicos}
}

\parskip=5pt % 10pt es el tamao de fuente

% Pongo en 0 la distancia extra entre temes.
\let\olditemize\itemize
\def\itemize{\olditemize\itemsep=0pt}

% Acomodo fancyhdr.
\pagestyle{fancy}
\thispagestyle{fancy}
\addtolength{\headheight}{1pt}
\lhead{Algoritmos y Estructuras de Datos II}
\rhead{$1^{\mathrm{er}}$ cuatrimestre de 2012}
\cfoot{\thepage /\pageref{LastPage}}
\renewcommand{\footrulewidth}{0.4pt}

\author{Algoritmos y Estructuras de Datos II, DC, UBA.}
\date{}
\title{Tipos abstractos de datos bsicos}

\begin{document}

%Hay que preguntar como formateamos esto
% \textbf{TAD} Timestamp \textbf{es} Nat \\
% semana = 604800

%Pais, nombre, Tags... etc hace falta decir que son strings?

\section{Aclaraciones}
Decidimos tomar como par\'ametro del TAD $Mundo$ el tipo param\'etrico $Pa\mbox{\'i}s$ y para el TAD $Red Social$ los tipos param\'etricos $Pa\mbox{\'i}s$, $Usuario$ y $Tiempo$, con el fin de no imponer restricciones arbitrarias sobre ellos.
A este \'ultimo, de todos modos, es necesario pedirle que posea orden y que posea una operaci\'on ``restarUnaSemana($t$)'' que tome una instancia del tipo $Tiempo$ y devuelva otra que represente el mismo momento pero una semana atr\'as,
con el fin de poder decidir correctamente el contenido del muro de un usuario.\\

El formato de un mensaje decidimos modelarlo como un TAD enumerado, al igual que, por ejemplo, el TAD b\'asico $Bool$.\\

Por \'ultimo, tomamos la decisi\'on de que no se puedan agregar pa\'ises despu\'es de generada una instancia inicial de $Red Social$, ya que no entraba en contradicci\'on con el enunciado y simplificaba significativamente el TAD.

\newpage

\section{Renombres}

\textbf{TAD} Etiqueta \textbf{es} $String$

\textbf{TAD} FormatoMensaje \textbf{es} enumerado de \{texto, audio, video, imagen\}

\textbf{TAD} Mensaje(Usuario, Tiempo$_{\leq}$) \textbf{es} Tupla(Usuario, Tiempo, FormatoMensaje, conj(Etiqueta))

\textbf{donde} $\prod_1$ \textbf{es} $usuario$ \textbf{,} $ \prod_2$ \textbf{es} $tiempo$ \textbf{,} 
$ \prod_3$ \textbf{es} $formato$ \textbf{y} $ \prod_4$ \textbf{es} $etiquetas$


\section{TAD \tadNombre{Redsocial(pais, usuario, tiempo$_{\leq}$)}}

\begin{tad}{\tadNombre{Redsocial(pais, usuario, tiempo$_{\leq}$)}}
  
   
   \tadIgualdadObservacional{r_1}{r_2}{redsocial}{
$(mundo(r_1) \igobs mundo(r_2)) \wedge$\\
$(mensajes(r_1) \igobs mensajes (r_2)) \wedge$\\
$(usuarios(r_1) \igobs usuarios(r_2))\ \yluego$\\ 
$ (\forall u:usuarios(r_1))$\\
$(((solicitudesEnviadas(r_1,u) \igobs$\\$ solicitudesEnviadas(r_2,u)) \wedge $
$(nacionalidad(r_1,u) \igobs nacionalidad(r_2,u)))$\\}
   \tadAlinearFunciones{enviarSolicitud}{mundo/m,pais/p_1,pais/p_1,tipo}

  \tadParametrosFormales{
    \tadEncabezadoInline{g\'eneros}{pais, usuario, tiempo}
  }
  \tadGeneros{redsocial(pais, usuario, tiempo)}
  \tadExporta{redsocial(pais, usuario, tiempo), generadores, observadores, amigos, muro, cuantosDecora, ultimoMensaje}
  \tadUsa{\tadNombre{Bool, Mundo, conj(pais), conj(usuario), conj(mensaje)}}

  \tadAlinearFunciones{registrarUsuario}{redsocial/r,usuario/u_1,usuario/u_2}

  \tadGeneradores
  \tadOperacion{nuevaRed}{mundo}{redsocial}{}
  \tadOperacion{registrarUsuario}{redsocial/r,usuario/u,pais/p}{redsocial}{$u \not\in$ usuarios($r$) $\wedge$ $p \in$ paises(mundo($r$))}
  \tadOperacion{publicar}{redsocial/r,mensaje/m}{redsocial}{ usuario($m$) $\in$ usuarios($r$) $\wedge$ ($\emptyset?$(mensajes($r$)) $\oluego$ tiempo($m$) $\geq$ tiempo(ultimoMensaje($r$))) }
  \tadOperacion{enviarSolicitud}{redsocial/r,usuario/u_1,usuario/u_2}{redsocial}{ $u_1 \not= u_2$ $\wedge\ \{u_1,u_2\} \subseteq$ usuarios($r$) 
$\yluego\ u_2 \not\in$ solicitudesEnviadas($r$,$u_1$) }

  %agregar observador nombre a cada apariencia de usuario donde corresponda, ya que consideramos al usuario como una dupla de nombre y nacionalidad

  \tadObservadores
  \tadAlinearFunciones{solicitudesEnviadas}{redsocial/r,usuario/u}
  \tadOperacion{mundo}{redsocial}{mundo}{}
  \tadOperacion{usuarios}{redsocial}{conj(usuario)}{}
  \tadOperacion{mensajes}{redsocial}{conj(mensaje)}{}
  \tadOperacion{nacionalidad}{redsocial/r,usuario/u}{pais}{$u \in$ usuarios($r$)}
  \tadOperacion{solicitudesEnviadas}{redsocial/r,usuario/u}{conj(usuario)}{$u \in$ usuarios($r$)}

  \tadOtrasOperaciones
  %Exportables
  \tadAlinearFunciones{solicitudesEnviadas}{redsocial/r,mensaje/m,conj(mensaje)/ms}

  \tadOperacion{amigos}{redsocial/r,usuario/u}{conj(usuario)}{$u \in$ usuarios($r$)}
  \tadOperacion{muro}{redsocial/r,usuario/u}{conj(mensaje)}{$u \in$ usuarios($r$)}
  \tadOperacion{cuantosDecora}{redsocial/r,usuario/u,etiqueta}{Nat}{$u \in$ usuarios($r$)}
  \tadOperacion{ultimoMensaje}{redsocial/r}{mensaje}{$\neg  \emptyset?$(mensajes($r$))}
  
  %No exportables
  \tadOperacion{ultimosMensajesDe}{redsocial/r,usuario/u}{conj(mensaje)}{$u \in$ usuarios($r$)}
  \tadOperacion{filtrarMensajes}{redsocial/r,usuario/u,conj(mensajes)/ms}{conj(mensaje)}{$u \in$ usuarios($r$) $\wedge$ $ms \subseteq$ mensajes($r$)}
  \tadOperacion{amigosAux}{redsocial/r,usuario/u,conj(usuario)/us}{conj(usuario)}{$u \in$ usuarios($r$) $\wedge\ us \subseteq$ solicitudesEnviadas($r, u$)}
  \tadOperacion{ultimoMensajeAux}{redsocial/r,mensaje/m,conj(mensaje)/ms}{mensaje}{$m \in$ mensajes($r$) $\wedge\ ms\ \subseteq$ mensajes($r$)}
  \tadOperacion{muroSinBloqueos}{redsocial/r,conj(usuario)/us}{conj(mensaje)}{$us \subseteq$ usuarios($r$)}
  \tadOperacion{aplicarBloqueos}{redsocial/r,conj(mensaje)/ms,pais/p}{conj(mensaje)}{$p \in$ paises(mundo($r$)) $\wedge$
									    ($\forall m \in ms$)($\exists u \in$ usuarios($r$))$\ m \in$ ultimosMensajesDe($u$)}
  \tadOperacion{contarDecoraciones}{etiqueta,conj(mensaje)}{Nat}{}
  \tadOperacion{$\beta$}{bool}{Nat}{}

  \tadAxiomas[\paratodo{mundo}{m}, \paratodo{redsocial}{r}, \paratodo{pais}{p}, \paratodo{usuario}{u,u_1,u_2,uarg}, 
  \paratodo{conj(usuario)}{us}, \paratodo{mensaje}{m}, \paratodo{conj(mensaje)}{ms}, \paratodo{etiqueta}{e}, \paratodo{bool}{expresion}]

  \tadAlinearAxiomas{solicitudesEnviadas(enviarSolicitud($r, u_1, u_2$), $uarg$)}

  \tadAxioma{mundo(nuevaRed($m$))}{$m$}
  \tadAxioma{mundo(registrarUsuario($r, u, p$))}{mundo($r$)}
  \tadAxioma{mundo(publicar($r, m$))}{mundo($r$)}
  \tadAxioma{mundo(enviarSolicitud($r, u_1, u_2$))}{mundo($r$)}
  
  \tadAxioma{usuarios(nuevaRed($m$))}{$\emptyset$}
  \tadAxioma{usuarios(registrarUsuario($r, u, p$))}{Ag($u$, usuarios($r$))}
  \tadAxioma{usuarios(publicar($r, m$))}{usuarios($r$)}
  \tadAxioma{usuarios(enviarSolicitud($r, u_1, u_2$))}{usuarios($r$)}
  
  \tadAxioma{mensajes(nuevaRed($m$))}{$\emptyset$}
  \tadAxioma{mensajes(registrarUsuario($r, u, p$))}{mensajes($r$)}
  \tadAxioma{mensajes(publicar($r, m$))}{Ag($m$, mensajes($r$))}
  \tadAxioma{mensajes(enviarSolicitud($r, u_1, u_2$))}{mensajes($r$)}

  \tadAxioma{nacionalidad(registrarUsuario($r, u, p$), $uarg$)}{\IF $u\ =\ uarg$
								THEN $p$
								ELSE nacionalidad($r, uarg$)
								FI}
  \tadAxioma{nacionalidad(publicar($r, m$), $uarg$)}{nacionalidad($r, uarg$)}
  \tadAxioma{nacionalidad(enviarSolicitud($r, u_1, u_2$), $uarg$)}{nacionalidad($r, uarg$)}
  
  \tadAxioma{solicitudesEnviadas(registrarUsuario($r, u, p$), $uarg$)}{\IF $u\ =\ uarg$
								THEN $\emptyset$
								ELSE solicitudesEnviadas($r, uarg$)
								FI}
  \tadAxioma{solicitudesEnviadas(publicar($r, m$), $uarg$)}{solicitudesEnviadas($r$)}
  \tadAxioma{solicitudesEnviadas(enviarSolicitud($r, u_1, u_2$), $uarg$)}{\IF $u_1\ =\ uarg$
								THEN Ag($u_2$, solicitudesEnviadas($r, uarg$))
								ELSE solicitudesEnviadas($r, uarg$)
								FI}

   \tadAlinearAxiomas{ultimoMensajeAux($r, m, ms$)}
 
   \tadAxioma{amigos($r, u$)}{amigosAux($r, u$, solicitudesEnviadas($r, u$))}

   \tadAxioma{amigosAux($r, u, us$)}{\IF us\ =\ $\emptyset$
				    THEN $\emptyset$
				    ELSE
					{\IF $u \in$ solicitudesEnviadas($r$, dameUno($us$)) 
					THEN Ag(dameUno($us$), amigosAux($r, u$, sinUno($us$)))
					ELSE amigosAux($r, u$, sinUno($us$))
					FI}
				    FI}

   \tadAxioma{ultimoMensaje($r$)}{ultimoMensajeAux($r$,dameUno(mensajes($r$)),sinUno(mensajes($r$)))}

   \tadAxioma{ultimoMensajeAux($r, m, ms$)}{\IF $\emptyset$?($ms$)
					   THEN	$m$
					   ELSE
						{\IF tiempo($m$) $\leq$ tiempo(dameUno($ms$))
						THEN ultimoMensajeAux($r$, dameUno($ms$), sinUno($ms$))
						ELSE ultimoMensajeAux($r, m$, sinUno($ms$))
						FI}
					  FI}

   \tadAxioma{muro($r, u$)}{aplicarBloqueos($r$, muroSinBloqueos($r$, amigos($u$)), nacionalidad($r, u$))}
   
   \tadAxioma{muroSinBloqueos($r, us$)}{\IF $\emptyset?(us)$
				      THEN $\emptyset$
				      ELSE ultimosMensajesDe($r$, dameUno($us$)) $\cup$ \\
					   muroSinBloqueos($r$, sinUno($us$))
				      FI}

   \tadAxioma{aplicarBloqueos($r, ms, p$)}{\IF $\emptyset?(ms)$
					 THEN $\emptyset$
					 ELSE {\IF estaBloqueado(mundo($r$), nacionalidad($r$, usuario(dameUno($ms$))), $p$, formato(dameUno($ms$))
					      THEN aplicarBloqueos($r$, sinUno($ms$), $p$)
					      ELSE Ag(dameUno($ms$), aplicarBloqueos($r$, sinUno($ms$), $p$)) 
					      FI}
					 FI}

   \tadAxioma{ultimosMensajesDe($r,u$)}{filtrarMensajes($r, u$, mensajes($r$))}

   %falta signatura%
   \tadAxioma{estaEnLaSemana?($r, m$)}{tiempo(ultimoMensaje($r$)) $\leq$ Semana 
					  $\oluego$ restarUnaSemana(tiempo(ultimoMensaje($r$)), Semana) $\leq$ tiempo($m$)}
   
   \tadAxioma{filtrarMensajes($r, u, ms$)}{\IF $\emptyset?(ms)$
					THEN $\emptyset$
					ELSE{\IF $u =$ usuario(dameUno($ms$)) $\wedge$ estaEnLaSemana?($r$,dameUno($ms$)) 
					    THEN Ag(dameUno($ms$),filtrarMensajes($r$, sinUno($ms$)))
					    ELSE filtrarMensajes($r$, sinUno($ms$))
					    FI}
					FI}

   \tadAxioma{cuantosDecora($r, u, e$)}{contarDecoraciones($e$, muro($r,u$))}
   \tadAxioma{contarDecoraciones($e, ms$)}{\IF $\emptyset?(ms)$
 					THEN 0
 					ELSE$\beta$($e \in$ etiquetas(dameUno($ms$))) + contarDecoraciones($e$, sinUno($ms$))
 					FI}
   \tadAxioma{$\beta$($expresion$)}{IF $expresion$ 
				 THEN $1$
				 ELSE $0$ 
				 FI}

\end{tad}

\section{TAD \tadNombre{Mundo(pais)}}

\begin{tad}{\tadNombre{Mundo(pais)}}
  
  \tadIgualdadObservacional{m_1}{m_2}{mundo}{$(paises(m_1) \igobs paises(m_2))\ \yluego$\\ $(\forall t:formatomensaje)(\forall p \in paises(m_1))$\\
$bloqueos(m_1,p,t) \igobs bloqueos(m_2,p,t) $}

  \tadParametrosFormales{
    \tadEncabezadoInline{g\'eneros}{pais}
  }
  \tadGeneros{mundo(pais)}
  \tadExporta{mundo(pais), generadores, observadores, estaBloqueado, permitidos, bloqueosConsistentes}
  \tadUsa{\tadNombre{Bool, conj(pais)}}

  \tadAlinearFunciones{bloqueosConsistentes}{mundo/m,pais/p_1,pais/p_2,formatomensaje}

  \tadGeneradores
  \tadOperacion{nuevo}{conj(pais)}{mundo}{}
  \tadOperacion{bloquear}{mundo/m,pais/p_1,pais/p_2,formatomensaje}{mundo}{$p_1 \not= p_2$ $\wedge\ \{p_1,p_2\} \subseteq$ paises($m$)}

  %agregar observador nombre a cada apariencia de usuario donde corresponda, ya que consideramos al usuario como una dupla de nombre y nacionalidad

  \tadObservadores
  \tadOperacion{paises}{mundo}{conj(pais)}{}
  \tadOperacion{bloqueos}{mundo/m,pais/p,formatomensaje}{conj(pais)}{$p \in$ paises($m$)}

  %tipo es una enumarcion de texto, imagen, video, audio

  \tadOtrasOperaciones
  \tadOperacion{estaBloqueado}{mundo/m,pais/p_1,pais/p_2,formatomensaje}{bool}{$p_1 \not= p_2$ $\wedge\ \{p_1,p_2\} \subseteq$ paises($m$)}
  \tadOperacion{permitidos}{mundo/m,pais/p,formatomensaje}{conj(pais)}{$p \in$ paises($m$)}
  \tadOperacion{bloqueosConsistentes}{mundo}{bool}{}


  \tadOperacion{bloqueosConsPaises}{mundo/m,conj(pais)/ps,formatomensaje}{bool}{$ps \subseteq$ paises($m$)}

  \tadAlinearFunciones{paisConsistente}{mundo/m,conj(pais)/bs,conj(pais)/ps,formatomensaje}
  \tadOperacion{paisConsistente}{mundo/m,conj(pais)/bs,conj(pais)/ps,formatomensaje}{bool}{$bs \subseteq$ paises($m$) $\wedge\ ps \subseteq$ paises($m$)}


  % Tipo es una enumarcion de video, audio, foto y texto (puede ser int tambien).
  %  \tadOperacion{vaca?}{secu($\alpha$)}{bool}{}
  %  \tadOperacion{prim}{secu($\alpha$)/s}{$\alpha$}{$\neg$ vaca?($s$)}
  %  \tadOperacion{fin}{secu($\alpha$)/s}{secu($\alpha$)}{$\neg$ vaca?($s$)}
  \tadAxiomas[\paratodo{mundo}{m}, \paratodo{conj(pais)}{ps}, \paratodo{pais}{p,p_1,p_2,parg}, \paratodo{formatomensaje}{fm,fmarg}]

  \tadAlinearAxiomas{bloqueos(bloquear($m$,$p_1$,$p_2$,$fm$),$parg$,$fmarg$)}



  \tadAxioma{paises(nuevo($ps$))}{$ps$}
  \tadAxioma{paises(bloquear($m$,$p_1$,$p_2$,$fm$))}{paises($m$)}

  \tadAxioma{bloqueos(nuevo($ps$),$parg$,$fmarg$)}{$\emptyset$}
  \tadAxioma{bloqueos(bloquear($m$,$p_1$,$p_2$,$fm$),$parg$,$fmarg$)}{\IF $parg = p_1 \wedge fmarg = fm$ 
								      THEN Ag($p_2$,bloqueos($m$,$parg$,$fmarg$)) 
								      ELSE bloqueos($m$,$parg$,$fmarg$) FI}

  \tadAxioma{estaBloqueado($m$,$p_1$,$p_2$,$fm$)}{$p_2 \in\ $bloqueos($m$,$p_1$,$fm$)}
  \tadAxioma{permitidos($m$,$p$,$fm$)}{paises($m$) $-$ bloqueos($m$,$p$,$fm$) }

  \tadAxioma{bloqueosConsistentes($m$)}{bloqueosConsPaises($m$, paises($m$), $texto$) $\wedge$\\
					bloqueosConsPaises($m$, paises($m$), $audio$) $\wedge$\\
					bloqueosConsPaises($m$, paises($m$), $video$) $\wedge$\\
					bloqueosConsPaises($m$, paises($m$), $imagen$)}

  \tadAxioma{bloqueosConsPaises($m, ps, fm$)}{\IF $\emptyset?(ps)$
						 THEN $True$
						 ELSE paisConsistente($m$, bloqueos($m$, dameUno($ps$), $fm$),\\
						 permitidos($m$, dameUno($ps$), $fm$), $fm$) $\wedge$ \\
						 bloqueosConsPaises($m$, sinUno($ps$), $fm$)
						 FI}

  \tadAlinearAxiomas{paisConsistente($m, bloqueados, permitidos, fm$)}


  \tadAxioma{paisConsistente($m, bloqueados, permitidos, fm$)}{\IF $\emptyset?(ps)$
					  THEN $True$
					  ELSE ($bloqueados \subseteq$ \\ bloqueos($m$, dameUno($permitidos$), $fm$))
					  $\wedge$ \\  paisConsistente($m, bloqueos$,\\sacarUno($permitidos$), $fm$)
					  FI}
  

\end{tad}

% NO HACE FALTA! LEER MAIL DE PABLO HEIBER
% 
% 
% 
% \section{TAD \tadNombre{FormatoMensaje}}
% 
% \begin{tad}{\tadNombre{FormatoMensaje}}
%   \tadGeneros{formatomensaje}
%   \tadExporta{}
%   
%   \tadIgualdadObservacionalSimple{
% $(texto \igobs texto) \land \neg(texto \igobs audio) \land \neg(texto \igobs video) \land \neg(texto \igobs imagen)$\\
% $ \land (audio \igobs audio) \land \neg(audio \igobs texto) \land \neg(audio \igobs video) \land \neg(audio \igobs imagen)$\\
% $ \land (video \igobs video) \land \neg(video \igobs audio) \land \neg(video \igobs texto) \land \neg(video \igobs imagen)$\\
% $ \land (imagen \igobs imagen) \land \neg(imagen \igobs audio) \land \neg(imagen \igobs video) \land \neg(imagen \igobs texto)$\\
% }
% 
%   \tadGeneradores
%   \tadOperacion{texto}{}{formatomensaje}{}
%   \tadOperacion{audio}{}{formatomensaje}{}
%   \tadOperacion{video}{}{formatomensaje}{}
%   \tadOperacion{imagen}{}{formatomensaje}{}
% 
% 
% \end{tad}


\end{document}
